<h2>Proof development for Separation Algebras,
Share Accounting, and Indirection Theory
<p>
Andrew W. Appel, Robert Dockins, Aquinas Hobor
<p>
July 2009
<p>
See the SUMMARY file for an explanation.
Note in particular the HOW TO BUILD section.
<p>
LICENSE:  Starting in 2022, MSL is licensed as part of
the Verified Software Toolchain.  The BSD-2-clause
license (for VST) is in the parent directory.
  
</h2>
